Section: New Results

Proving equivalence between probabilistic programs

Participants : Benjamin Grégoire, Gilles Barthe [IMDEA] , Steve Kremer [Inria Nancy Grand-Est, PESTO project Team] , Pierre-Yves Strub [Ecole Polytechnique] .

We have developed principled methods for proving equivalence between probabilistic programs that operate over finite fields and related algebraic structures. We have focused on three essential properties: program equivalence, information flow, and uniformity. We give characterizations of these properties based on deducibility and other notions from symbolic cryptography. We use (sometimes improve) tools from symbolic cryptography to obtain decision procedures or sound proof methods for program equivalence, information flow, and uniformity. A partial implementation of our approach is integrated in EasyCrypt and in MaskVerif. This work has been published at an international conference [6].